Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		a__filter(cons(X,Y),0,M)	→ cons(0,filter(Y,M,M))
2:		a__filter(cons(X,Y),s(N),M)	→ cons(mark(X),filter(Y,N,M))
3:		a__sieve(cons(0,Y))	→ cons(0,sieve(Y))
4:		a__sieve(cons(s(N),Y))	→ cons(s(mark(N)),sieve(filter(Y,N,N)))
5:		a__nats(N)	→ cons(mark(N),nats(s(N)))
6:		a__zprimes	→ a__sieve(a__nats(s(s(0))))
7:		mark(filter(X1,X2,X3))	→ a__filter(mark(X1),mark(X2),mark(X3))
8:		mark(sieve(X))	→ a__sieve(mark(X))
9:		mark(nats(X))	→ a__nats(mark(X))
10:		mark(zprimes)	→ a__zprimes
11:		mark(cons(X1,X2))	→ cons(mark(X1),X2)
12:		mark(0)	→ 0
13:		mark(s(X))	→ s(mark(X))
14:		a__filter(X1,X2,X3)	→ filter(X1,X2,X3)
15:		a__sieve(X)	→ sieve(X)
16:		a__nats(X)	→ nats(X)
17:		a__zprimes	→ zprimes

There are 16 dependency pairs:


18:		A__FILTER(cons(X,Y),s(N),M)	→ MARK(X)
19:		A__SIEVE(cons(s(N),Y))	→ MARK(N)
20:		A__NATS(N)	→ MARK(N)
21:		A__ZPRIMES	→ A__SIEVE(a__nats(s(s(0))))
22:		A__ZPRIMES	→ A__NATS(s(s(0)))
23:		MARK(filter(X1,X2,X3))	→ A__FILTER(mark(X1),mark(X2),mark(X3))
24:		MARK(filter(X1,X2,X3))	→ MARK(X1)
25:		MARK(filter(X1,X2,X3))	→ MARK(X2)
26:		MARK(filter(X1,X2,X3))	→ MARK(X3)
27:		MARK(sieve(X))	→ A__SIEVE(mark(X))
28:		MARK(sieve(X))	→ MARK(X)
29:		MARK(nats(X))	→ A__NATS(mark(X))
30:		MARK(nats(X))	→ MARK(X)
31:		MARK(zprimes)	→ A__ZPRIMES
32:		MARK(cons(X1,X2))	→ MARK(X1)
33:		MARK(s(X))	→ MARK(X)

Consider the SCC {18-33}. The constraints could not be solved.

Tyrolean Termination Tool (7.49 seconds) --- May 3, 2006